i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(k:{k:Knd| 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(k:{(k  ks)} 
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(decl-state
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:((ds)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(ma-valtype
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:((da; k)
i:Id, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), x:Id, T:Type, v:T, ks:(Knd List), tr:(TT).
fpf-compatible(Id; x.Type; id-deq; ds; fpf-single(x; T))
 normal-type{i:l}
 normal-type(T)
 (k:Knd. (k  ks)  (isrcv(k))  (i = destination(lnk(k))))
 normal-ds{i:l}
 normal-ds(ds)
 normal-da{i:l}
 normal-da(da)
 R-realizes{i:l}
 R-realizes(R-state-var-init(i; ds; da; x; T; v; ks; tr);
 R-realizes(es.(es-decls(es;i;ds;da)
 R-realizes( (es-dtype(es; i; x; T)
 R-realizes( c alle-at(es;
 R-realizes( c alle-at(i;
 R-realizes( c alle-at(e.((es-after(es; x; e)
 R-realizes( c alle-at(e.((=
 R-realizes( c alle-at(e.((es-trans-state-from{i:l}(es;ks;tr;v;es-init(es;e);e)
 R-realizes( c alle-at(e.(( T)
 R-realizes( c alle-at( ((es-first(es; e))  (es-when(es; x; e) = v  T))))))) 

latex

Definitions

subtype(S; T), es-dtype(es; i; x; T), R-state-var-init(i; ds; da; x; T; v; ks; tr), Rinit-v(x1), Reffect-f(x1), Rinit-discrete(A), Rinit-x(x1), Rinit?(x1), Reffect-discrete(A), ff, Rsends-T(x1), Reffect-T(x1), Rsends-dt(x1), Rpre-a(x1), Rpre-ds(x1), Rpre?(x1), Rsends-ds(x1), Rbframe-L(x1), Rbframe-k(x1), Rbframe?(x1), Rsframe-L(x1), Rsends-knd(x1), Rsends-g(x1), Rsframe-tag(x1), Rsends-l(x1), Rsframe-lnk(x1), Rsframe?(x1), Rsends?(x1), Rrframe-L(x1), Reffect-ds(x1), Rrframe-x(x1), Rrframe?(x1), Raframe-L(x1), Raframe-k(x1), Raframe?(x1), Rframe-L(x1), Reffect-knd(x1), Reffect-x(x1), Rframe-x(x1), Rframe?(x1), Reffect?(x1), tt, t.2, t.1, (i = j), band(p; q), R-interface-compat(A; B), R-discrete_compat(A; B), R-frame-compat(A; B), R-base-domain(R), eq_bd(p; q), Rda(R), Rds(R), R-loc(R), True, Rnone?(x1), Rplus-right(x1), Rplus-left(x1), Rplus?(x1), if b then t else f fi , Y, R-compat{i:l}(A; B), P  Q, P  Q, P  Q, top, decl-type{i:l}(ds; x), decl-state(ds), R-state-var(i; ds; da; x; T; ks; tr), guard(T), sq_type(T), P  Q, es-le(es; e; e'), e'e.P(e'), alle-at(es; i; e.P(e)), A c B, x. t(x), prop{i:l}, t  T, P  Q, x:A. B(x), init-p(es; i; T; x; v), Unit, , ma-valtype(da; k), x(s),

Lemmas

es-discrete-when-first, es-when-init, assert of null, or functionality wrt iff, assert of bor, null wf3, bor wf, es-init-le, es-E wf, es-first wf, es-loc-init, es-init wf, es-loc wf, alle-at wf, es-isconst wf, Rplus wf, R-implies-rule, not wf, bnot wf, fpf-empty wf, Kind-deq wf, fpf-empty-compatible-right, bool wf, eq id wf, not functionality wrt iff, assert of bnot, eqff to assert, fpf-empty-compatible-left, fpf-compatible-self, fpf-single wf, fpf-compatible-symmetry, fpf-compatible-join, assert-eq-id, eqtt to assert, iff transitivity, R-compat-Rall, fpf-cap-single1, fpf-compatible-join-cap, fpf-cap-join-subtype, subtype rel self, top wf, fpf-cap wf, subtype rel dep function, Rframe wf, decl-type wf, fpf-join wf, Reffect wf, Rall wf, R-compat-Rplus2, R-compat-symmetry, es-when wf, es-isrcv wf, es-trans-state-from wf, es-decls-iff, es-vartype wf, es-le-loc, Id sq, es-after wf, es-locl wf, fpf wf, ma-valtype wf, decl-state wf, fpf-single wf3, id-deq wf, fpf-compatible wf, normal-type wf, lnk wf, ldst wf, Id wf, isrcv wf, assert wf, l member wf, Knd wf, normal-ds wf, normal-da wf, init-p wf, rationals wf, Rinit wf, R-state-var wf, R-and-rule, R-init-rule, R-state-var-rule